/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transl;

import java.io.BufferedOutputStream;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.PrintWriter;
import java.util.Iterator;
import java.util.List;

import alloy.ast.ASTDepthFirstVisitor;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryFormula;
import alloy.ast.BinaryIntExpr;
import alloy.ast.CardinalityExpr;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.DeclIter;
import alloy.ast.ElemFormula;
import alloy.ast.ElemIntFormula;
import alloy.ast.EmptyFormula;
import alloy.ast.EmptySetExpr;
import alloy.ast.ExprCastIntExpr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.IdentityExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IfThenElseIntExpr;
import alloy.ast.ImplicationFormula;
import alloy.ast.LiteralIntExpr;
import alloy.ast.LogicOp;
import alloy.ast.Multiplicity;
import alloy.ast.MultiplicityExpr;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.QuantifiedExpr;
import alloy.ast.QuantifiedFormula;
import alloy.ast.SetMultExpr;
import alloy.ast.SigExpr;
import alloy.ast.SumExpr;
import alloy.ast.SumIntExpr;
import alloy.ast.UnaryExpr;
import alloy.ast.UniversalExpr;
import alloy.ast.VarCreator;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.bool.BoolSwitch;
import alloy.bool.BooleanFormula;
import alloy.type.BasicType;
import alloy.type.RelationType;
import alloy.util.Dbg;
import alloy.util.Mapper;

/**
 * Write out the translatable AST as XML, for regression testing / comparison between
 * different Alloy versions.
 */
public class TranslOutputXMLVisitor extends ASTDepthFirstVisitor {
    /**
     * An optional user-provided node annotator: for each node,
     * provides an attribute string to add to that node's XML.
     * representation.
     */
    private Mapper _nodeAnnotator;

    /** Writer to the XML file we're writing. */
    PrintWriter w;

    /////////////
    // Methods //
    /////////////
	
    
    private TranslOutputXMLVisitor(String fname) throws FileNotFoundException {
	w = new PrintWriter(new BufferedOutputStream(new FileOutputStream(fname)));
	w.println("<?xml version='1.0' encoding='utf-8'?>");
    }
    
    private void close() { w.close(); }

    /**
     * Write out the given Formula to an XML file.
     * @param nodeAnnotator_ optional user-defined node annotator: for each {@link Node} returns
     *    an attribute string to add to that node's XML representation.  May be null, then no
     *    attributes are added.
     */
    public static void writeXML(Node n_, String fname_, Mapper nodeAnnotator_) {
	try {
	    TranslOutputXMLVisitor v = new TranslOutputXMLVisitor(fname_);
	    v._nodeAnnotator = nodeAnnotator_;
	    n_.applyVisitor(v);
	    v.close();
	} catch (FileNotFoundException e_) {
	    System.out.println("Could not write translatable AST as XML to " + fname_ + " : " + e_);
	}
    }

    /* Replace "sole" with "lone" for compatibily with Alloy 3 */
    private static String _sole2lone(String x) {
        return x.equals("sole") ? "lone" : x;
    }

    /** Return an optional node annotation, or an empty string if none. */
    private String _annot(Node n_) { 
        StringBuffer annot = new StringBuffer(_nodeAnnotator != null ? (" "
                + (String) _nodeAnnotator.map(n_) + " ") : "");
        alloy.ast.Location loc = n_.getLocation();
        if (loc.getFileName() != null) {
            annot.append(" file=\"" + loc.getFileName() + "\" begLine=\""
                    + loc.getBeginLine() + "\" begCol=\""
                    + loc.getBeginColumn() + "\" endLine=\"" + loc.getEndLine()
                    + "\" endCol=\"" + loc.getEndColumn() + "\" ");
        }
        if (n_.getAnnotation() != null && n_.getAnnotation().length() > 0)
            annot.append(" note=\"" + n_.getAnnotation() + "\" ");

        if (n_.getTransformAnnotation() != null
                && n_.getTransformAnnotation().length() > 0)
            annot.append(" transformNote=\"" + n_.getTransformAnnotation()
                    + "\" ");

        return annot.toString();
    }
    
    /**************/
    /*** Leaves ***/
    /**************/
    
    
    /** Translate as a relation */
    public void visit(SigExpr sigExpr_) {
        w.print("<Rel name=\"" + sigExpr_.toString() + "\"" + _annot(sigExpr_) + "/>");
    }
    /** Translate as a relation */
    //    public void visit(FieldExpr fieldExpr_) {
    //	w.print("<Rel name=\"" + fieldExpr_.toString() + "\"/>");
    //}
    
    /** If this refers to a field, translate as a relation;
	otherwise, allocate an {@link ExprTransl} of switchable constants. */
    public void visit(VariableExpr variableExpr_) {
		if (variableExpr_.isQuantified)
		    w.print("<QVar name=\"" + variableExpr_.toString() + "\"" + _annot(variableExpr_) + "/>");
		else
		    w.print("<Rel name=\"" + variableExpr_.toString() + "\"" + _annot(variableExpr_) + "/>");
    }

    /****************/
    /*** Formulas ***/
    /****************/

    public void visit(ElemFormula elemFormula_) {
	    String opName = "";
		CompOp op = elemFormula_.getOp();
		if (op.isNegated()) {
		    opName = "not_";
		    op = op.negation();
		}
		opName += (op.equals(CompOp.SUBSETCOLON) || op.equals(CompOp.SUBSETIN)) ? "in" : "equals";
		w.println("<ElemFormula op=\"" + opName + "\"" + _annot(elemFormula_) + ">");
		elemFormula_.getLeft().applyVisitor(this);
		elemFormula_.getRight().applyVisitor(this);
		w.println("</ElemFormula>");
    }

    /** Implicitly conjoined {@link alloy.ast.Formula}s. */
    public void visit(FormulaSeq formulaSeq_) {
        _visitConjunction(formulaSeq_);
    }

    public void visit(Node node_) { Dbg.fatal("untranslated node: " + node_); }

    /** Treat as constant TRUE. */
    public void visit(EmptyFormula emptyFormula_) {
        w.println("<True " + _annot(emptyFormula_) + "/>");
    }

    private void _visitConjunction(Formula f) {
		List /* of Formula */ flatConjuncts = GatherConjoinedFormulasVisitor.gatherConjoinedFormulas(f);
		if (flatConjuncts.size() == 0)
		    w.println("<True " + _annot(f) + "/>");
		else {
		    if (flatConjuncts.size() != 1)
			w.println("<And " + _annot(f) + ">");
		    for (Iterator conjIter = flatConjuncts.iterator(); conjIter.hasNext();) {
			Formula conj = (Formula)conjIter.next();
			conj.applyVisitor(this);
		    }
		    if (flatConjuncts.size() != 1)
			w.println("</And>");
		}
    }

    private void _visitDisjunction(Formula f) {
		List /* of Formula */ flatDisjuncts = GatherDisjoinedFormulasVisitor.gatherDisjoinedFormulas(f);
		if (flatDisjuncts.size() == 0)
		    w.println("<False " + _annot(f) + "/>");
		else {
		    if (flatDisjuncts.size() != 1)
			w.println("<Or " + _annot(f) + ">");
		    for (Iterator disjIter = flatDisjuncts.iterator(); disjIter.hasNext();) {
			Formula disj = (Formula)disjIter.next();
			disj.applyVisitor(this);
		    }
		    if (flatDisjuncts.size() != 1)
			w.println("</Or>");
		}
    }

    public void visit(BinaryFormula binaryFormula_) {
		if (binaryFormula_.getOp().equals(LogicOp.AND)) {
		    _visitConjunction(binaryFormula_);
		} else if (binaryFormula_.getOp().equals(LogicOp.OR)) {
		    _visitDisjunction(binaryFormula_);
		} else {
		    w.println("<Iff " + _annot(binaryFormula_) + ">");
		    binaryFormula_.getLeft().applyVisitor(this);
		    binaryFormula_.getRight().applyVisitor(this);
		    w.println("</Iff>");
		}
    }

    public void visit(ImplicationFormula implFormula_) {
		w.println("<IfThenElse " + _annot(implFormula_) + ">");
		implFormula_.getIfFormula().applyVisitor(this);
		implFormula_.getThenFormula().applyVisitor(this);
		implFormula_.getElseFormula().applyVisitor(this);
		w.println("</IfThenElse>");
    }

    public void visit(NegFormula negFormula_) {
		w.println("<Not " + _annot(negFormula_) + ">");
		negFormula_.getFormula().applyVisitor(this);
		w.println("</Not>");
    }

    public void visit(QuantifiedExpr quantExpr_) {
		w.println("<QuantExpr quant=\"" + _sole2lone(quantExpr_.getQuantifier().nodeString()) + "\"" + _annot(quantExpr_) + ">");
		quantExpr_.getExpr().applyVisitor(this);
		w.println("</QuantExpr>");
    }

    /** Write XML representation of the given {@link BasicType} */
    private void writeXML(BasicType basicType_) {
        w.print("<BasicType name=\"" + basicType_.toString() + "\"/>");
    }

    /** Write XML representation of the given {@link RelationType} */
    private void writeXML(RelationType relType_) {
		w.print("<RelType>");
		for (int i=0; i<relType_.numBasicTypes(); i++)
		    writeXML(relType_.getBasicTypeAt(i));
		w.print("</RelType>");
    }

    /** Write XML representation of multiplicity expression */
    private void writeXML(MultiplicityExpr multExpr_) {
// 	MultiplicityExpr multExpr = multExpr_;
// 	if (multExpr instanceof SetMultExpr) {
// 	    SetMultExpr setMultExpr = (SetMultExpr)multExpr;
// 	    w.println("<SetMult>");
// 	    w.println("<SetMultiplicity>" + setMultExpr.getSetMult().nodeString() + "</SetMultiplicity>");
// 	    w.println("<SetMultExpr>");
// 	    setMultExpr.getExpr().applyVisitor(this);
// 	    w.println("</SetMultExpr>");
// 	    w.println("</SetMult>");
// 	} else {
// 	    ArrowMultExpr arrowMult = (ArrowMultExpr)multExpr;
// 	    RelMultiplicity leftMult = arrowMult.getLeftMult();
// 	    RelMultiplicity rightMult = arrowMult.getRightMult();
	    
// 	    w.println("<ArrowMult>");
// 	    w.println("<ArrowMultLeft mult=\"" + leftMult.nodeString() + "\">");
// 	    arrowMult.getLeft().applyVisitor(this);
// 	    w.println("</ArrowMultLeft>");
// 	    w.println("<ArrowMultRight mult=\"" + rightMult.nodeString() + "\">");
// 	    arrowMult.getRight().applyVisitor(this);
// 	    w.println("</ArrowMultRight>");
	    
// 	    w.println("</ArrowMult>");
// 	}
    }

    /**
     * Write XML representation of the quantified variable declarations
     * in the given {@link VarCreator}.
     */
    private void writeXML(VarCreator varCreator_) {
		for (DeclIter declIter = new DeclIter(varCreator_); declIter.hasNext();) {
		    declIter.next();
		    Variable var = declIter.getVariable();
		    MultiplicityExpr mult = declIter.getMultiplicity();
		    String multName = "";
		    if (mult instanceof SetMultExpr) {
			SetMultExpr setMultExpr = (SetMultExpr)mult;
			if (!setMultExpr.getMult().equals(Multiplicity.NONE))
			    multName = " mult=\"" + setMultExpr.getMult() + "\"";
		    }
		    w.println("<Var name=\"" + var.nodeString() + "\" " + multName +  "/>");
		    //writeXML(declIter.getType());
		}
    }

    public void visit(SumIntExpr sumIntExpr_) {
		w.println("<SumIntExpr " + _annot(sumIntExpr_) + ">");
		writeXML(sumIntExpr_);  // write the quantified variable declarations
		w.println("<SumIntExprBody>");
		sumIntExpr_.getBody().applyVisitor(this);
		w.println("</SumIntExprBody>");
		w.println("</SumIntExpr");
    }  // visit(sumIntExpr_)
    
    public void visit(QuantifiedFormula quantForm_) {
		w.println("<QuantForm quant=\"" + _sole2lone(quantForm_.getQuantifier().nodeString()) + "\"" + _annot(quantForm_) + ">");
		writeXML(quantForm_);  // write the quantified variable declarations
		quantForm_.getBody().applyVisitor(this);
		w.println("</QuantForm>");
    }  // visit(QuantifiedFormula ...)
    
    /** Translate a {@link ComprehensionExpr} to an {@link ExprTransl}.
	For each bit of the {@link ExprTransl}, we construct a
	{@link BooleanFormula} which sets the {@link BoolSwitch}es of
	the quantified variables in this comprehension to values corresponding to the
	coordinates of the bit.
     */
    public void visit(ComprehensionExpr compExpr_) {
		w.println("<Compreh " + _annot(compExpr_) + ">");
		writeXML(compExpr_);  // write the quantified variable declarations
		compExpr_.getBody().applyVisitor(this);
		w.println("</Compreh>");
    }  // visit(ComprehensionExpr)

    /*************/
    /*** Exprs ***/
    /*************/

    public void visit(BinaryExpr binaryExpr_) {
		w.println("<BinaryExpr op=\"" + binaryExpr_.getOp() + "\"" + _annot(binaryExpr_) + ">");
		binaryExpr_.getLeft().applyVisitor(this);
		binaryExpr_.getRight().applyVisitor(this);
		w.println("</BinaryExpr>");
    }

    public void visit(UniversalExpr univExpr_) {
		w.println("<UnivExpr " + _annot(univExpr_) + "/>");
		//writeXML(univExpr_.getType());
		//w.println("</UnivExpr>");
    }
    public void visit(EmptySetExpr emptyExpr_) {
		w.println("<NoneExpr " + _annot(emptyExpr_) + "/>");
		//writeXML(emptyExpr_.getType());
		//w.println("</NoneExpr>");
    }

    public void visit(IdentityExpr idenExpr_) {
		w.println("<IdenExpr " + _annot(idenExpr_) + "/>");
		//writeXML(idenExpr_.getType());
		//w.println("</IdenExpr>");
    }

    public void visit(UnaryExpr unaryExpr_) {
		w.println("<UnaryExpr op=\"" + unaryExpr_.getOp() + "\"" + _annot(unaryExpr_) + ">");
		unaryExpr_.getExpr().applyVisitor(this);
		w.println("</UnaryExpr>");
    }

    public void visit(IfThenElseExpr ifThenElseExpr_) {
		w.println("<IfThenElseExpr " + _annot(ifThenElseExpr_) + ">");
		ifThenElseExpr_.getIfFormula().applyVisitor(this);
		ifThenElseExpr_.getThenExpr().applyVisitor(this);
		ifThenElseExpr_.getElseExpr().applyVisitor(this);
		w.println("</IfThenElseExpr>");
    }
    
    /****************/
    /*** IntExprs ***/
    /****************/

    public void visit(LiteralIntExpr literalIntExpr_) {
        w.println("<LiteralInt val=\"" + literalIntExpr_.getVal() + "\" "+ _annot(literalIntExpr_) + "/>");
    }

    public void visit(ElemIntFormula elemIntFormula_) {
		w.println("<ElemIntFormula op=\"" + elemIntFormula_.getOp() +  "\"" + _annot(elemIntFormula_) + ">");
		elemIntFormula_.getLeft().applyVisitor(this);
		elemIntFormula_.getRight().applyVisitor(this);
		w.println("</ElemIntFormula>");
    }

    public void visit(BinaryIntExpr intExpr_) {
		w.println("<BinaryIntExpr op=\"" + intExpr_.getOp() +  "\"" + _annot(intExpr_) + ">");
		intExpr_.getLeft().applyVisitor(this);
		intExpr_.getRight().applyVisitor(this);
		w.println("</BinaryIntExpr>");
    }

    public void visit(CardinalityExpr cardExpr_ ) {
		w.println("<CardinalityExpr " + _annot(cardExpr_) + ">");
		cardExpr_.getExpr().applyVisitor(this);
		w.println("</CardinalityExpr>");
    }

    public void visit(IfThenElseIntExpr ifThenElseIntExpr_) {
		w.println("<IfThenElseIntExpr " + _annot(ifThenElseIntExpr_) + ">");
		ifThenElseIntExpr_.getIfFormula().applyVisitor(this);
		ifThenElseIntExpr_.getThenIntExpr().applyVisitor(this);
		ifThenElseIntExpr_.getElseIntExpr().applyVisitor(this);
		w.println("</IfThenElseIntExpr>");
    }

    public void visit(SumExpr sumExpr_) {
		w.println("<SumExpr " + _annot(sumExpr_) + ">");
		sumExpr_.getExpr().applyVisitor(this);
		w.println("</SumExpr>");
    }

    public void visit(ExprCastIntExpr sumExpr_) {
		w.println("<ExprCastIntExpr " + _annot(sumExpr_) + ">");
		sumExpr_.getExpr().applyVisitor(this);
		w.println("</ExprCastIntExpr>");
    }

}
